Pre/post-conditions annotations using Rust expressions#57
Merged
Conversation
coord-e
force-pushed
the
coord-e/annotation-v2
branch
from
809279c to
89fc507
Compare
This was referenced Mar 30, 2026
Merged
coord-e
force-pushed
the
coord-e/annotation-v2
branch
from
89fc507 to
2958eb1
Compare
coord-e
changed the title
coord-e
force-pushed
the
coord-e/annotation-v2
branch
2 times, most recently
from
ec48146 to
97f139c
Compare
This was referenced Apr 30, 2026
coord-e
force-pushed
the
coord-e/annotation-v2
branch
5 times, most recently
from
50bcc1b to
a46e74d
Compare
There was a problem hiding this comment.
Pull request overview
Adds a new thrust-macros proc-macro crate that lets users write #[thrust_macros::requires(<rust-expr>)] / #[thrust_macros::ensures(<rust-expr>)], expanding them into thrust::formula_fn-backed annotations (as introduced in #65). The PR also updates injected specs (std.rs) and UI tests to use the new expression-based annotation style, and wires the driver to pass --extern thrust_macros=... automatically.
Changes:
- Introduce
thrust-macrosproc-macro crate implementingrequires/ensuresvia generated#[thrust::formula_fn]helper functions. - Update
std.rsextern specs and UI tests to use Rust-expression annotations (including*x/!xconventions for mutable models). - Convert repo to a workspace and update the driver (
src/main.rs) to locate and link thethrust_macrosproc-macro dylib at runtime.
Reviewed changes
Copilot reviewed 13 out of 16 changed files in this pull request and generated 6 comments.
Show a summary per file
| File | Description |
|---|---|
| thrust-macros/src/lib.rs | Implements the proc-macros and code generation for requires/ensures via formula_fn. |
| thrust-macros/Cargo.toml | Defines the new proc-macro crate. |
| thrust-macros/Cargo.lock | Adds a per-crate lockfile for thrust-macros. |
| src/main.rs | Adds runtime detection + --extern injection for thrust_macros. |
| std.rs | Migrates injected extern specs to the new Rust-expression annotation style. |
| tests/ui/pass/tuple_annot.rs | Updates passing UI test to thrust_macros::{requires,ensures} syntax. |
| tests/ui/pass/annot_mut_term.rs | Updates passing UI test to Mut::new(...) expression syntax. |
| tests/ui/pass/annot_exists.rs | Updates passing UI test to `exists( |
| tests/ui/pass/annot_enum_simple.rs | Updates passing UI test with Model + PartialEq to support expression-based equality. |
| tests/ui/fail/* | Updates failing UI tests to the new macro-based syntax. |
| Cargo.toml | Turns repo into a workspace; adds thrust-macros dependency to ensure it is built. |
| Cargo.lock | Records thrust-macros as a dependency in the workspace lock. |
| .gitignore | Adjusts ignore pattern for target/. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Change thrust-macros expansion for extern_spec_fn functions When the annotated function already has #[thrust::extern_spec_fn], inject requires_path/ensures_path into the original function body instead of generating a separate _thrust_extern_spec_ wrapper. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> Replace thrust::trusted with thrust::ignored on the original fn in requires/ensures expansion Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
coord-e
force-pushed
the
coord-e/annotation-v2
branch
from
91d78fd to
0803ff0
Compare
3 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Introduce thrust-macros crate, and thrust_macros::requires and thrust_macros::ensures expands to annotations using thrust::formula_fn introduced in #65